A:Type, I:MaInterface(A), i:{i:Id| (i  fpf-domain(I))} , k:{k:Knd| (k  fpf-domain(I(i).2))} .
(I(i).2(k).1)  Type 

latex

Definitions	Id, MaInterface(T), Top, a:A fp B(a), t  T, x:AB(x), x:A. B(x), fpf-domain(f), (x  l), {x:A| B(x)} , Knd, Type, IdDeq, f(x), t.2, x:A  B(x), hasloc(k;i), b, , x.A(x), x. t(x), KindDeq, P  Q, t.1, P  Q, P & Q, P  Q, type List, s = t, S  T
Lemmas	ma-interface-type-trivial, member-fpf-domain-variant, pi1 wf, fpf-ap wf, Knd wf, top wf, Kind-deq wf, fpf-trivial-subtype-set, assert wf, hasloc wf, ma-interface-da-type0, l member wf, fpf-domain wf